YES 15.915000000000001 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((elemIndex :: Float  ->  [Float ->  Maybe Int) :: Float  ->  [Float ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



Lambda Reductions:
The following Lambda expression
\vv1
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((elemIndex :: Float  ->  [Float ->  Maybe Int) :: Float  ->  [Float ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((elemIndex :: Float  ->  [Float ->  Maybe Int) :: Float  ->  [Float ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,i if p x then i : [] else []
findIndices00 p _ []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((elemIndex :: Float  ->  [Float ->  Maybe Int) :: Float  ->  [Float ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p _ []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((elemIndex :: Float  ->  [Float ->  Maybe Int) :: Float  ->  [Float ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : vxJust a



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndex :: Float  ->  [Float ->  Maybe Int) :: Float  ->  [Float ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : vxJust a



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule List
  (elemIndex :: Float  ->  [Float ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : vxJust a



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wz5300), Succ(wz400000)) → new_primPlusNat(wz5300, wz400000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(wz3100), Succ(wz40100)) → new_primMulNat(wz3100, Succ(wz40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(wz123, Succ(wz18000), Succ(wz22500), wz224) → new_psPs(wz123, wz18000, wz22500, wz224)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Succ(wz1820), wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs1(wz125, Succ(wz1820), wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Succ(wz1810), wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Succ(wz1810), wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
QDP
                                    ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
QDP
                                        ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ QReductionProof
QDP
                                            ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs2(wz143, Succ(wz1850), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr1(wz45, wz430, :(wz4610, wz4611), wz143) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_psPs3(wz143, Succ(wz1860), wz430, Pos(wz46010), wz45, :(wz4610, wz4611)) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_foldr2(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz144, wz143) → new_psPs3(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs2(wz143, Succ(wz1850), wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr2(wz45, wz430, Float(Pos(wz46000), wz4601), wz461, wz144, wz143) → new_psPs2(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs3(wz143, Succ(wz1860), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
QDP
                                    ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs2(wz143, Succ(wz1850), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr1(wz45, wz430, :(wz4610, wz4611), wz143) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_psPs3(wz143, Succ(wz1860), wz430, Pos(wz46010), wz45, :(wz4610, wz4611)) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_foldr2(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz144, wz143) → new_psPs3(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs2(wz143, Succ(wz1850), wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr2(wz45, wz430, Float(Pos(wz46000), wz4601), wz461, wz144, wz143) → new_psPs2(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs3(wz143, Succ(wz1860), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)

The TRS R consists of the following rules:

new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ DependencyGraphProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs4(wz121, Succ(wz1770), wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Succ(wz1780), wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))
new_psPs4(wz121, Succ(wz1770), wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Succ(wz1780), wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
QDP
                                    ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
QDP
                                        ↳ QReductionProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ QReductionProof
QDP
                                            ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr6(wz310, wz4110, wz4111, wz223, wz222) → new_foldr5(wz310, wz4111, wz222)
new_foldr5(wz310, :(wz4110, wz4111), wz127) → new_foldr6(wz310, wz4110, wz4111, new_primPlusNat0(wz127, Succ(Zero)), new_primPlusNat0(wz127, Succ(Zero)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr8(wz45, wz430, Float(Pos(wz46000), wz4601), :(wz4610, wz4611), wz146, wz145) → new_foldr8(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz145, Succ(Zero)), new_primPlusNat0(wz145, Succ(Zero)))
new_foldr8(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz146, wz145) → new_foldr7(wz45, wz430, wz461, wz145)
new_foldr7(wz45, wz430, :(wz4610, wz4611), wz145) → new_foldr8(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz145, Succ(Zero)), new_primPlusNat0(wz145, Succ(Zero)))

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr10(wz310, Float(Neg(wz41000), wz4101), wz411, wz124, wz123) → new_foldr9(wz310, wz411, wz123)
new_foldr9(wz310, :(wz4110, wz4111), wz123) → new_foldr10(wz310, wz4110, wz4111, new_primPlusNat0(wz123, Succ(Zero)), new_primPlusNat0(wz123, Succ(Zero)))
new_foldr10(wz310, Float(Pos(wz41000), wz4101), wz411, wz124, wz123) → new_foldr9(wz310, wz411, wz123)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr11(wz82, wz800, :(wz8310, wz8311), wz175) → new_foldr12(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz175, Succ(Zero)), new_primPlusNat0(wz175, Succ(Zero)))
new_foldr12(wz82, wz800, Float(Pos(wz83000), wz8301), :(wz8310, wz8311), wz176, wz175) → new_foldr12(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz175, Succ(Zero)), new_primPlusNat0(wz175, Succ(Zero)))
new_foldr12(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz176, wz175) → new_foldr11(wz82, wz800, wz831, wz175)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs6(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz174, wz173) → new_psPs7(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Succ(wz1880), wz800, Pos(wz83010), wz82, :(wz8310, wz8311)) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_foldr13(wz82, wz800, :(wz8310, wz8311), wz173) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_psPs7(wz173, Succ(wz1890), wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs6(wz173, Succ(wz1880), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Pos(wz83000), wz8301), wz831, wz174, wz173) → new_psPs6(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Succ(wz1890), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)

The TRS R consists of the following rules:

new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
QDP
                                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs6(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz174, wz173) → new_psPs7(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Succ(wz1880), wz800, Pos(wz83010), wz82, :(wz8310, wz8311)) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_foldr13(wz82, wz800, :(wz8310, wz8311), wz173) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_psPs7(wz173, Succ(wz1890), wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs6(wz173, Succ(wz1880), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Pos(wz83000), wz8301), wz831, wz174, wz173) → new_psPs6(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Succ(wz1890), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))

The set Q consists of the following terms:

new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: